COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.<< For a summary of features, see LET.DOC[1,LES] >>
C00009 00003	∂CSL 29 August 1980$Director, Defense Advanced Research Projects Agency
C00016 ENDMK
C⊗;
.<< For a summary of features, see LET.DOC[1,LES] >>
.ONR←"Resident Representative, O.N.R."&
.  "↓Room 165, Durand Building↓Stanford University↓Stanford, California 94305";
.
.ARPA←"Advanced Research Projects Agency↓"&
.  "1700 Wilson Boulevard↓Arlington, Virginia 22209";
.
.IPT←"Information Processing Techniques Office↓"&
.  "Advanced Research Projects Agency↓"&
.  "1700 Wilson Boulevard↓Arlington, Virginia 22209";
.
.TURN ON "%{α"
.height←53;
.device xgp;
.  page frame height high 85 wide
.  title area heading lines 1 to 10 char 1 to 80;
.  area text lines 4 to height char 1 to 80;
.
.  font 1 "basl30"; font 2 "basi30"; font 3 "basb30";
.  AT "ffi" ⊂ IF 0<THISFONT≤3 THEN "≠"  ELSE "fαfαi" ⊃;
.  AT "ffl" ⊂ IF 0<THISFONT≤3 THEN "α∞" ELSE "fαfαl" ⊃;
.  AT "ff"  ⊂ IF 0<THISFONT≤3 THEN "≥"  ELSE "fαf" ⊃;
.  AT "fi"  ⊂ IF 0<THISFONT≤3 THEN "α≡" ELSE "fαi" ⊃;
.  AT "fl"  ⊂ IF 0<THISFONT≤3 THEN "∨"  ELSE "fαl" ⊃;
.  AT "--"  ⊂ IF 0<THISFONT≤3 THEN "¬" ELSE "-α-" ⊃;
.
.fntlst←"456789ABCDEFG";
.n←0;			<< font # gensym >>
.recursive macro defont(fnm);	⊂ start
.  if declaration(fnm)=0 then start
.    n←n+1;	fnm←fnt←fntlst[n];
.    font fnt "fnm";
.    end
.   else fnt←fnm;
.  end ⊃;
.
.at "↓";	⊂ break ⊃;
.
.macro letter(data,aut);	⊂
.<< namad = date$to$from$subject$ccs>>
.ODDLEFTBORDER←EVENLEFTBORDER←1000;
.every heading();
.if going=0 then going←1 else next page;
.nofill;
.count page from 2;
.sss←"data";  foo←scan(sss," ","","XR");  dat←scan(sss,"$","","is");
.xxx←namad←scan(sss,"$","","IS");
.zzz←scan(xxx,"↓","","IS");	if 2<length(xxx)<5 then namad←zzz&"↓"&eval(xxx);
.author←scan(sss,"$","","is");	if length(author)<2 then author←"aut";
.subject←scan(sss,"$","","is");	ccs←sss;
.place heading;
. ⊃
.
.macro head(spc);	⊂ place text; nofill; select 1; group skip spc;
.begin at "; " ⊂ break ⊃;
.(namad)}
.end
.subj;
.fill adjust;
.every heading(%3{dat},,Page {page!});
.⊃
.
.macro memo(spc);	⊂ place text; begin "memo"
.at "; " ⊂ break⊃;
.fill; nojust; indent 8,8; crbreak; tabs 9; turn on "\%"; preface 0;
.group skip spc;
.xxx←namad;  nam←scan(xxx,"↓");
.once indent 0,8;
%3To:\%1{nam}
.skip;
.if length(ccs) then start
.once indent 0,8;
%3Cc: \%1{ccs}
.skip;
.end
.once indent 0,8;
%3From:\%1{author}

.end "memo";
.subj;
.fill adjust; skip;
.every heading(%3{dat},,Page {page!});
.⊃
.
.macro subj;	⊂
.fac; preface 1;
.if length(subject)>2 then BEGIN "subject"
.turn on "%∂"; nojust;
.indent 0,8;
%3Subject:∂9%1{subject}

.end "subject";
.select 1;
.  ⊃
.
.macro ref ⊂ select 3; nojust; boldit;
References:
.count ref inline; at "⊗" ⊂next ref; ("["&ref&"]  ");⊃
.select 1; indent 0,8;
. ⊃
.
.macro sgn; ⊂ BEGIN "signed" nofill; group;narrow 50;
.at "; ";	⊂ }
.⊃;
.SKIP;
Best regards,
.skip 3
{author}
.END "signed";
.cclist;
.  ⊃
.
.macro cclist	⊂ if length(ccs) then begin fill nojust
.turn on "∂";
.preface 0; skip;
.at "; "	⊂ break ⊃;
.indent 3,8;
.once indent 0,3;
cc: ∂4{ccs}

. end
.⊃
.
.macro sin; ⊂ BEGIN "signed" nofill; group;narrow 50;
.at "; ";	⊂ }
.⊃;
.SKIP;
Sincerely,
.skip 3
{author}
.END "signed";
.cclist;
.  ⊃
.
.macro signed(aut); ⊂ BEGIN "signed" nofill; group;narrow 50;
.at "; ";	⊂ }
.⊃;
.SKIP 2;
aut
.END "signed";
.cclist
.  ⊃
.
.MACRO FAC ⊂ FILL ADJUST ⊃
.MACRO FAD ⊂ FILL ADJUST double space; preface 2; ⊃
.macro BS  ⊂ BEGIN INDENT 0,3; PREFACE SPREAD-1; NOJUST ⊃
.
.macro cb(head) ⊂ if lines<5 then skip 200;
.once turn on "←"; select 3
←head

.⊃
.macro begit	⊂ begin fill crbreak preface 0; indent 0,4; tabs 5; turn on "\";
.  ⊃
.macro boldit ⊂ turn on "%";
.  at """" ⊂ (if thisfont=1 then "%3" else "%1") ⊃;
.  at "<" ⊂"%2"⊃; at ">" ⊂"%1"⊃;
.⊃
.
.at "∂CSL" data "∞"; ⊂
.letter(|data|,|John McCarthy; Professor of Computer Science|);
.begin turn on "→"
.defont("STAN2");  defont("NGB25");  select stan2;
S{("%"&ngb25)}Computer Science Department, STANFORD UNIVERSITY, Stanford, California 94305
Telephone 415 497-4330 →{dat}
.  end
.head(4);
.xgenlines←xgenlines-4;
.⊃
.
.going←0;
.portion main;  place text;
.preface 1;
∂CSL 29 August 1980$Director, Defense Advanced Research Projects Agency
↓Department of Defense↓Washington, D. C.$John McCarthy↓Professor of Computer Science
$Quarterly Management Report∞

.every heading("%3Director, DARPA","{dat}","Page {page!}");
.font A "ngr20"
.begin "barf"
.nofill
.at "<" ⊂"%3"⊃; at ">" ⊂"%1"⊃;
.turn on "→\"
.tabs 4,42,46
→%AForm approved, Budget
→Bureau No. 22-RO293.%*

<ARPA Order Number:> 2494\<Contract Number:> MDA903-80-C-0102

<Program Code Number:> 2D338\<Principal Investigator:> Prof. John McCarthy
\\\415 497-4430

<Name of Contractor:>  Board of Trustees of the Leland Stanford Junior University

<Effective Date of Contract:> 1 October 1979\<Short Title of Work:> Computer Science
\\\Research
<Contract Expiration Date:> 30 September 1981

<Amount of Contract:>  $817,872
.end "barf"
.skip

Dear Sir:

Recent external publications of our staff have been on formal reasoning [Reference
11], program verification [14, 15], and advanced computer architectures [12, 13].
Members of our staff recently published
Ph.D. dissertations on formal reasoning [1, 8], knowledge-based reasoning [3, 5],
and robotics [9].
Other reports appeared on mathematical theory of computation [2],
computer graphics [4], formal reasoning [6], and a text editor [7].

.cb Research Program and Plan

No change.

.cb Major Accomplishments

None.

.cb Problems Encountered

Nothing new.

.cb Fiscal Status

.begin turn on "→"
Amount currently funded:→$305,000

Estimated expenditures and commitments (through 30 June 1980): →$189,656

Estimated funds required to complete the work (through 30 September 1981): →$817,872
.end

.cb Action Required by the Government

None.

.cb Future Plans

No change.

.sgn; skip 2;
cc: addressee - 2 copies, John McCarthy, Robert Kahn (ARPA), ONR Stanford.

.if lines<15 then next page else skip;
.cb REFERENCES

.INDENT 0,3; NOJUST; TURN ON "%α";
.AT """" ⊂ (IF THISFONT=1 THEN "%3" ELSE "%1") ⊃
.AT "<" ⊂ "%2" ⊃;  AT ">" ⊂ "%1" ⊃;
.AT "AIM-" ⊂ "Stanford A. I. Memo AαIαMα-" ⊃;

.COUNT exref TO 200
.AT "⊗" ⊂ IF LINES<3 THEN NEXT PAGE; NEXT EXREF; (EXREF&".  ") ⊃

⊗David E.  Wilkins,
"Using Patterns and Plans to Solve Problems and Control Search",
Thesis: PhD in Computer Science,
AIM-329, June 1979.

⊗Zohar Manna and Amir Pnueli, 
"The Modal Logic of Programs", AIM-330, September 1979.

⊗Elaine Kant,
"Efficiency Considerations in Program Synthesis: A Knowledge-Based Approach",
Thesis: PhD in Computer Science, AIM-331, July 1979.

⊗Donald E. Knuth, 
"METAFONT, a system for alphabet design",
AIM-332, September 1979.

⊗Brian McCune,
"Building Program Models Incrementally from Informal Descriptions",
Thesis: PhD in Computer Science, AIM-333, October 1979.

⊗John McCarthy, 
"Circumscription - A Form of Non-Monotonic Reasoning",
AIM-334, February 1980.

⊗Arthur Samuel, 
"Essential E", AIM-335, March 1980.

⊗Martin Brooks,
"Determining Correctness by Testing",
Thesis: PhD in Computer Science, AIM-336, May 1980.

⊗Morgan Ohwovoriole,
"An Extention of Screw Theory and its Application to the Automation of
Industrial Assemblies",
Thesis: PhD in Mechanical Engineering, AIM-338, April 1980.

⊗Aiello, Luigia and G. Prini, "Design of a personal computing system",
<Proc. Annual Conf. of the Canadian 
Information Processing Society>, Victoria (British Columbia), May 12-14,
1980.

⊗Goad, Chris, "Proofs as descriptions of computations", <Proc. Automatic 
Deduction Conference>, Les Arcs (France), July 8-11, 1980.

⊗Moravec, Hans P., "Fully Interconnecting Multiple Computers with
Pipelined Sorting Nets", <IEEE Trans. on Computers>, October 1979.

⊗Moravec, Hans, "The Endless Frontier and The Thinking Machine",
<The Endless Frontier>, Vol. 2,
Jerry Pournelle, ed., Grosset & Dunlap, Ace books, 1980. (to appear)

⊗Nelson, C.G. and Oppen, D., "Simplification by Cooperating Decision
Procedures", <ACM Transactions on Programming Languages
and Systems>, Oct. 1979.

⊗Polak, Wolfgang, "An exercise in automatic program verification",
<IEEE Trans. on Software Engineering>, vol. SE-5, Sept. 1979.